$\forall$$x$:Id, $k$:Knd, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$a$:Knd fp$\rightarrow$ Top, $f$:Top, $x_{1}$:Id, $t$:Type, $v$:$t$.
\\[0ex]${\it ds}$ $\parallel$ $x_{1}$ : $t$
\\[0ex]$\Rightarrow$ (with declarations ds:${\it ds}$da:${\it da}$effect of $k$(v) is $x$ := $f$ s v $\Vert\!+$ $x_{1}$ : $t$ initially $x_{1}$ = $v$)